M:MsgA, k:Knd, l:IdLnk, tg:Id. M.sframe(k sends <l,tg>)   

latex

Definitions	x:A. B(x), t  T, , M.sframe(k sends <l,tg>), t.1, t.2, x. t(x), x,y. t(x;y), MsgA, x(s), x(s1,s2)
Lemmas	fpf-val wf, IdLnk wf, Id wf, Knd wf, product-deq wf, idlnk-deq wf, id-deq wf, assert wf, deq-member wf, Kind-deq wf, fpf-dom wf, fpf-trivial-subtype-top, msga wf